The present invention relates to design optimization in formal verification and synthesis using approximate reachability analysis.
The proliferation of integrated circuits (ICs) has increasingly resulted in a demand for added functionalities in the designs of digital systems. The added functionalities may be implemented in ICs, in order to execute additional tasks in their respective applications or environments. These additional functionalities add to the complexity of the circuit. The increase in complexity gives rise to a need for advanced and complex formal techniques for verification and synthesis of circuit models.
One of the techniques used to optimize a circuit model for verification and synthesis is based on symbolic reachability analysis. Symbolic reachability analysis is carried out to identify design invariants in the circuit model. Design invariants are the properties of designs that do not change during the working of the design. A special form of a design invariant is known as a sequential constant. Sequential constants are outputs of sequential logic devices, such as flip-flops, which do not change their value during the execution of the design. One of the traditional methods for symbolic reachability analysis uses the Binary Decision Diagram (BDD) and Boolean Satisfiability (SAT).
The method for identifying invariants, using the above-mentioned technique, is expensive in terms of the time and resources needed. It limits the size of the design on which the technique can be used. The problem of scalability makes this technique unsuitable for use at the chip level of large circuits, and therefore restricts it to block-level designs with only a few thousand state bits. Therefore, the invariants, which come into existence due to the interaction of different blocks, cannot be detected by means of the conventional technique.
In light of the foregoing discussion, a need exists for a technique to identify design invariants that can be extended to the chip level. There is also a requirement for the application of design invariants in verification and synthesis. This would reduce the verification time and enable verification of assertions, without which the system could run out of resources. Moreover, there is an ongoing need to optimize circuits for space, timing and power requirements. The present invention addresses such a need.